T:Type, L1:T List, i, j:||L1||. swap(swap(L1;i;j);i;j) = L1 

latex

Definitions	ij, (i, j), P  Q, True, T, l[i], P  Q, , t  T, x:A. B(x), Prop, ||as||, P  Q, False, A, AB, P & Q, i  j < k, {i..j}, swap(L;i;j)
Lemmas	int seg wf, length wf1, swap length, le wf, list extensionality, swap wf, nat wf, swap select, select wf, squash wf, flip twice, flip wf, non neg length